Nuprl Lemma : gcd_p_neg_arg_2
2,24
postcript
pdf
a
,
b
,
y
:
. GCD(
a
;
b
;
y
)
GCD(
a
;-
b
;
y
)
latex
Definitions
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
GCD(
a
;
b
;
y
)
,
x
:
A
.
B
(
x
)
,
t
T
,
T
,
True
,
Prop
Lemmas
minus
minus
cancel
,
true
wf
,
squash
wf
,
gcd
p
neg
arg
,
gcd
p
wf
origin
a, b, y:
. GCD(a;b;y) 
GCD(a;-b;y) a, b, y:. GCD(a;b;y) GCD(a;-b;y) Q
Q Qx:A. B(x)
T
T